Justin Hsu
Approximate lifting is a concept from formal verification for reasoning about pairs of probabilistic programs, similar to an approximate notion of probabilistic couplings. Recently, we have explored an interesting connection: differential privacy is a consequence of a particular form of approximate lifting. This view yields a composition principle for differential privacy that is more general than standard composition, so that privacy for algorithms like Sparse Vector and the Exponential mechanism follow from an intuitive composition argument. In this talk we will present the connection in more detail and describe its implications both for formal verification of differential privacy and for the theory of differential privacy.
Joint with Gilles Barthe, Marco Gaboradi, Benjamin Gregoire, and Pierre-Yves Strub.